#include "PDTBoolVar.h"
#include "PDTCodeGraph.h"
#include "PDTZ3GraphVisitor.h"

PDTBoolVar::PDTBoolVar(PDTCodeGraph & CG, string name) :
  PDTExpBoolSing(CG), PDTVar(name)
{
  CG.addVar(this);
  cloneID = 0;
}

Z3_ast
PDTBoolVar::Z3NodeVisit (PDTZ3Visitor &ZV)
{
  if (Z3node != NULL)
    return Z3node;
  /*
   this->boolID++;
   const char * name = ZV.makeName(this->getName().c_str());
   Z3_symbol s  = Z3_mk_string_symbol(ZV.ctx, name);
   */

  char * name = makeUniqueName(getName().c_str());
  Z3_symbol s = Z3_mk_string_symbol(ZV.ctx, name);
  Z3node = Z3_mk_const(ZV.ctx, s, ZV.Var);

  return Z3node;
}
